Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		a(f,a(g,a(f,x)))	→ a(f,a(g,a(g,a(f,x))))
2:		a(g,a(f,a(g,x)))	→ a(g,a(f,a(f,a(g,x))))

There are 4 dependency pairs:


3:		A(f,a(g,a(f,x)))	→ A(f,a(g,a(g,a(f,x))))
4:		A(f,a(g,a(f,x)))	→ A(g,a(g,a(f,x)))
5:		A(g,a(f,a(g,x)))	→ A(g,a(f,a(f,a(g,x))))
6:		A(g,a(f,a(g,x)))	→ A(f,a(f,a(g,x)))

Consider the SCC {3-6}. The constraints could not be solved.

Tyrolean Termination Tool (0.05 seconds) --- May 4, 2006